﻿/************************************************************************
 * AIDE - Automata Identification Engine
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     AIDE\OfflineAlgo\DFAs\RPNI_MM.cs
 * Description  :     RPNI (Regular positive negative inference) for Mealy machines
 * Change log   :     -Oct 2013:  Initial version
 * To Do        :
 ************************************************************************/
using System;
using System.Collections.Generic;
using AIDE.Utils;
using SMLib.Automata.Base;
using SMLib.Automata.MM;

/// <summary>
/// Offline Learning algorithms for Mealy machines
/// </summary>
namespace AIDE.OfflineAlgo.NFMs
{
	/// <summary>
	/// RPNI (Regular positive negative inference) offline DFA learning algorithm
	/// <remarks>
	/// This implementation is based on ["Grammatical_Inference_Learning Automata and Grammars" (2010)]
	/// </remarks>
	/// </summary>
	public class RPNI_MM
	{
		/// <summary>
		/// A state with a Set of access string
		/// </summary>
		class Block
		{
			public Block (Sequence w)
			{
				this.elements = new List<Sequence> ();
				elements.Add (w);
				accepting = false;
			}

			public Block (List<Sequence> elements)
			{
				this.elements = elements;
				accepting = false;
			}

			public bool accepting;
			/// <summary>
			/// List of words in this block
			/// </summary>
			public List<Sequence> elements;

			public override string ToString ()
			{
				if (elements == null || elements.Count == 0)
					return "";
				return elements [0].ToString ();
			}

			public int ConsistantNumberOfChilds;
			public bool ConsisantAccepting;
		}

		/// <summary>
		/// Prefix Tree Accepting
		/// </summary>
		Tree<Block, PairOfSymbols> pta;
		/// <summary>
		/// Set of accepting (positive) and rejecting (negative) words
		/// </summary>
		List<Sequence> seqs;
		/// <summary>
		/// Input Alphabet
		/// </summary>
		Alphabet alph;
		/// <summary>
		/// set of blue and red nodes
		/// </summary>
		List<Tree<Block, PairOfSymbols>.TreeNode> redNodes, blueNodes, q_b_fathers, allNodes;

		public RPNI_MM (string path)
		{
			MM_Traces.ReadInputFile (path, ref seqs, ref alph);
		}

		/// <summary>
		/// Constructor
		/// </summary>
		public RPNI_MM (Alphabet alph, List<Sequence> seqs)
		{
			this.alph = alph;
			this.seqs = seqs;
		}

		/// <summary>
		/// Build the prefix tree acceptor
		/// </summary>
		void BuildPTA ()
		{
			Block b = new Block (new List<Sequence> ());
			b.elements.Add (new Sequence ());
			pta = new Tree<Block, PairOfSymbols> (new Tree<Block, PairOfSymbols>.TreeNode (b));

			allNodes = new List<Tree<Block, PairOfSymbols>.TreeNode> ();
			allNodes.Add (pta.Root);

			//myPTA = new DFA(alph);

			//* build the prefix tree out of positive samples
			foreach (Sequence w in seqs) {
				//* star from root
				Tree<Block, PairOfSymbols>.TreeNode root = pta.Root;
				Tree<Block, PairOfSymbols>.TreeNode curr = root;
				//* trace the nodes on tree
				for (int i = 0; i < w.Length; i++) {
					Tree<Block, PairOfSymbols>.TreeNode tmp = curr.ChildByEdge (w [i]);
					if (tmp == null) {
						for (int j = i; j < w.Length; j++) {
							curr.NodeObject.ConsistantNumberOfChilds++;

							Block bl = new Block (w.Prefix (j + 1));
							curr = curr.AddChild (bl, w [j]);
							allNodes.Add (curr);
						}
						Block blc = curr.NodeObject;
						blc.accepting = true;
						blc.ConsisantAccepting = true;
						break;
					} else
						curr = tmp;

					//* check if it is accepting
					if (i == w.Length - 1) {
						Block blc = curr.NodeObject;
						blc.accepting = true;
						blc.ConsisantAccepting = true;
					}
				}
			}

			//* initialize red node as root
			redNodes = new List<Tree<Block, PairOfSymbols>.TreeNode> ();
			redNodes.Add (pta.Root);

			//* initialize blue nodes as immediate successor of root
			blueNodes = new List<Tree<Block, PairOfSymbols>.TreeNode> ();
			foreach (Tree<Block, PairOfSymbols>.TreeNode r in pta.Root.Childs)
				blueNodes.Add (r);

			q_b_fathers = new List<Tree<Block, PairOfSymbols>.TreeNode> ();
			foreach (Tree<Block, PairOfSymbols>.TreeNode r in pta.Root.Childs)
				q_b_fathers.Add (pta.Root);
		}

		/// <summary>
		/// The learn function
		/// </summary>
		public MealyMachine Learn ()
		{
			Console.WriteLine ("RPNI algorithm for Mealy machines");
			Console.WriteLine ("Number of samples: " + seqs.Count);

			BuildPTA ();
			System.IO.File.WriteAllText ("RPNIMM_Tree.dot", pta.ExportAsDot ());

			while (blueNodes.Count != 0) {
				Tree<Block, PairOfSymbols>.TreeNode q_b, q_f;
				ChooseAndRemove (out q_b, out q_f);

				bool merged = false;
				foreach (Tree<Block, PairOfSymbols>.TreeNode q_r in redNodes) {

					int indexOfQb = 0;
					for (int i = 0; i < q_f.Childs.Count; i++)
						if (ReferenceEquals (q_f.Childs [i], q_b))
							break;
						else
							indexOfQb++;
					q_f.Childs [indexOfQb] = q_r;

					if (IsCompatible (q_b, q_r, q_f)) {
						//* confirm changes
						Confirm ();

						SelectBlueNodes (q_b);
						merged = true;
						break;
					} else {
						//* rollback chanes
						q_f.Childs [indexOfQb] = q_b;
						RollBack ();
					}
				}
				if (!merged)
					Promote (q_b);
			}

			MealyMachine conj = BuildConjecture ();

			Console.WriteLine ("Done! Size of machine:" + conj.Size + " Verifying the machine...");
			if (MM_Traces.Verify (conj, seqs))
				Console.WriteLine ("Failes!");
			else
				Console.WriteLine ("Machine is OK!");
			return conj;
		}
		#region -=[ UNDO ]=-
		void RollBack ()
		{
			foreach (Tree<Block, PairOfSymbols>.TreeNode q in allNodes) {
				while (q.Childs.Count != q.NodeObject.ConsistantNumberOfChilds) {
					q.Childs.RemoveAt (q.Childs.Count - 1);
					q.Edges.RemoveAt (q.Edges.Count - 1);
				}

				q.NodeObject.accepting = q.NodeObject.ConsisantAccepting;
			}
		}

		void Confirm ()
		{
			foreach (Tree<Block, PairOfSymbols>.TreeNode q in allNodes) {
				q.NodeObject.ConsistantNumberOfChilds = q.Childs.Count;
				q.NodeObject.ConsisantAccepting = q.NodeObject.accepting;
			}
		}
		#endregion
		/// <summary>
		/// Select blue nodes in each step.
		/// </summary>
		void SelectBlueNodes (Tree<Block, PairOfSymbols>.TreeNode removedNode)
		{

			for (int i = 0; i < allNodes.Count; i++) {
				if (ReferenceEquals (allNodes [i], removedNode)) {
					allNodes.RemoveAt (i);
					break;
				}
			}

			foreach (Tree<Block, PairOfSymbols>.TreeNode q in redNodes) {
				foreach (Tree<Block, PairOfSymbols>.TreeNode q_ch in q.Childs) {
					bool isRed = false;
					foreach (Tree<Block, PairOfSymbols>.TreeNode qr in redNodes)
						if (ReferenceEquals (qr, q_ch)) {
							isRed = true;
							break;
						}
					if (!isRed) {
						bool isBlue = false;
						foreach (Tree<Block, PairOfSymbols>.TreeNode qr in blueNodes)
							if (ReferenceEquals (qr, q_ch)) {
								isBlue = true;
								break;
							}
						if (!isBlue) {
							blueNodes.Add (q_ch);

							q_b_fathers.Add (q);
						}
					}
				}
			}
		}

		/// <summary>
		/// Build the conjecture in the last phase of algorithm
		/// </summary>
		/// <returns></returns>
		private MealyMachine BuildConjecture ()
		{
			MealyMachine myMM = new MealyMachine (alph);
			//int num=0;

			foreach (Tree<Block, PairOfSymbols>.TreeNode qr in redNodes) {
				myMM.AddState (new MealyMachine.Mealy_State (qr.NodeObject.ToString ()));
				//myMM.AddState (new MealyMachine.Mealy_State ((num++).ToString ()));
			}
			foreach (Tree<Block, PairOfSymbols>.TreeNode qr in redNodes) {
				MealyMachine.Mealy_State src = null;
				foreach (MealyMachine.Mealy_State st in myMM.GetStates()) {
					if (st.Identifier.Equals (qr.NodeObject.ToString ())) {
						src = st;
						break;
					}
				}
				for (int i = 0; i < qr.NumberOfChilds; i++) {
					MealyMachine.Mealy_State dst = null;
					foreach (MealyMachine.Mealy_State st in myMM.GetStates()) {
						if (st.Identifier.Equals (qr.Childs [i].NodeObject.ToString ())) {
							dst = st;
							break;
						}
					}
					if (dst != null) {
						MealyMachine.Mealy_Transition tr = new MealyMachine.Mealy_Transition (qr.Edges [i]);
						tr.SetDestination (dst);
						src.Transitions.Add (tr);
					}
				}
			}
            
			for (int i = 0; i < myMM.Size; i++)
				((MealyMachine.Mealy_State)myMM [i]).ChangeID (i.ToString ());

			return myMM;
		}

		/// <summary>
		/// Promote a node (from blue to red). Note that we already added the children of qp as blue nodes
		/// <remarks>
		/// Algorith 12.9, page 256
		/// </remarks>
		/// </summary>
		/// <param name="qp">the blue node</param>
		private void Promote (Tree<Block, PairOfSymbols>.TreeNode q_b)
		{
			//* make it red!
			redNodes.Add (q_b);
			//* add all chiled as blue
			blueNodes.AddRange (q_b.Childs);
			//* set their father as q_b
			foreach (Tree<Block, PairOfSymbols>.TreeNode h in q_b.Childs)
				q_b_fathers.Add (q_b);
		}

		/// <summary>
		/// Merge two nodes
		/// <remarks>
		/// Algorithm 12.11, page 257
		/// </remarks>
		/// </summary>
		/// <param name="q">a red node</param>
		/// <param name="qp">a blue node</param>
		/// <param name="q_f">father of qp</param>
		private void Merge (Tree<Block, PairOfSymbols>.TreeNode q_r, Tree<Block, PairOfSymbols>.TreeNode q_b, Tree<Block, PairOfSymbols>.TreeNode q_f)
		{
			Fold (q_r, q_b);
		}

		/// <summary>
		/// Fold two nodes
		/// <remarks>
		/// Algorithm 12.12, page 258
		/// </remarks>
		/// </summary>
		/// <param name="q">a red node</param>
		/// <param name="qp">being the root of a tree</param>
		private void Fold (Tree<Block, PairOfSymbols>.TreeNode q, Tree<Block, PairOfSymbols>.TreeNode qp)
		{
			Block bqp = qp.NodeObject;
			if (bqp.accepting) {
				Block bq = q.NodeObject;
				bq.accepting = true;
			}

			for (int i = 0; i < alph.Size; i++) {
				PairOfSymbols tr_qp_a;
				Tree<Block, PairOfSymbols>.TreeNode ch_qp_a = FindChildOf (qp, alph [i], out tr_qp_a);
				if (ch_qp_a == null)
					continue;

				PairOfSymbols tr_p_a;
				Tree<Block, PairOfSymbols>.TreeNode ch_q_a = FindChildOf (q, alph [i], out tr_p_a);

				if (ch_q_a != null) {
					if (tr_p_a.Output.Equals (tr_qp_a.Output)) {
						Fold (ch_q_a, ch_qp_a);
					} else {
						//* they are not compatible
						compat = false;
						return;
					}
				} else {
					//?????????????????????
					//ch_qp_a, tr_p_a???
					q.AddChild (ch_qp_a, tr_qp_a);
				}
			}
		}

		private Tree<Block, PairOfSymbols>.TreeNode FindChildOf (Tree<Block, PairOfSymbols>.TreeNode father, ISymbol input, out PairOfSymbols tr)
		{
			for (int i = 0; i < father.Edges.Count; i++) {
				PairOfSymbols e = father.Edges [i];
				if (e.Input.Equals (input)) {
					tr = e;
					return father.Childs [i];
				}
			}
			tr = null;
			return null;
		}

		bool compat;

		/// <summary>
		/// Check wheather two nodes are compatible or not, i.e. can we merge them (compatible) or not (incompatible)
		/// </summary>
		/// <param name="qp">the blue node</param>
		/// <param name="q">the red node</param>
		/// <returns></returns>
		private bool IsCompatible (Tree<Block, PairOfSymbols>.TreeNode q_b, Tree<Block, PairOfSymbols>.TreeNode q_r, Tree<Block, PairOfSymbols>.TreeNode q_f)
		{
			compat = true;
			Merge (q_r, q_b, q_f);

			if (!compat)
				return false;

			for (int h = 0; h < seqs.Count; h++) {
				Sequence testWord = seqs [h];
				Tree<Block, PairOfSymbols>.TreeNode cur = pta.Root;
				for (int i = 0; i < testWord.Length; i++) {
					PairOfSymbols tr;
					cur = this.FindChildOf (cur, testWord [i].Input, out tr);
					if (cur == null)
						break;
					//* seen an unexpected output!
					if (!tr.Output.Equals (testWord [i].Output)) {
						return false;
					}
				}
			}
			return true;
		}

		/// <summary>
		/// Choose the smallest blue node and remove it from the set of blue nodes
		/// </summary>
		/// <returns></returns>
		private void ChooseAndRemove (out Tree<Block, PairOfSymbols>.TreeNode q_b, out Tree<Block, PairOfSymbols>.TreeNode q_f)
		{
			//* select the minimum blue node
			//LexicoComparer.CurrentAlphabet = alph;
			WordsLexicoComparer comp = new WordsLexicoComparer (alph);
			Tree<Block, PairOfSymbols>.TreeNode min = blueNodes [0], minFather = q_b_fathers [0];
			int minIndex = 0;
			for (int i = 1; i < blueNodes.Count; i++) {
				if (comp.Compare (min.NodeObject.elements [0].InputProjection (), blueNodes [i].NodeObject.elements [0].InputProjection ()) > 0) {
					min = blueNodes [i];
					minFather = q_b_fathers [i];
					minIndex = i;
				}
			}
			//* remove it from blue node
			blueNodes.RemoveAt (minIndex);
			q_b_fathers.RemoveAt (minIndex);

			q_b = min;
			q_f = minFather;
		}
	}
}
